(TML)

  %Next, some theorems about APPEND, for later use as simprules %

let FIXAPPEND = FIX defAPPEND;;

let TAC = SUBSOCCSTAC[[1],FIXAPPEND] THEN SIMPTAC;;

let ss = itlist ssadd [NULLUUthm; NULLNILthm; NULLCONSthm;
                       HEADCONSthm; TAILCONSthm] BASICSS;;

let g = "APPEND UU L == UU";;

let gl,proof = TAC(g, ss, []);;

let  APPENDUUthm = proof[];;

hyp(APPENDUUthm);;


let g = "APPEND NIL L == L";;
let gl,proof = TAC(g,ss,[]);;
let APPENDNILthm = proof[];;
hyp(APPENDNILthm);;

let g = "APPEND(CONS A L)M == CONS A (APPEND L M)" ;;
let gl,proof = TAC(g,ss,[]) ;;
let APPENDCONSthm = proof[];;
hyp(APPENDCONSthm);;